/*
 * print_double(x) 的效果与 printf("%g", x) 一致，但旨在
 * 在所有平台上产生相同的格式。
 */
static void
print_double(double x)
{
#ifdef WIN32
	/* 将 Windows 的 3 位指数更改为看起来与其他人相同 */
	char		convert[128];
	int			vallen;

	sprintf(convert, "%g", x);
	vallen = strlen(convert);

	if (vallen >= 6 &&
		convert[vallen - 5] == 'e' &&
		convert[vallen - 3] == '0')
	{
		convert[vallen - 3] = convert[vallen - 2];
		convert[vallen - 2] = convert[vallen - 1];
		convert[vallen - 1] = '\0';
	}

	printf("%s", convert);
#else
	printf("%g", x);
#endif
}
